\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$:Type, $l_{1}$, $l_{2}$:IdLnk, ${\it tg}$, $a$:Id, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$Prop),\+
\\[0ex]$Q$:(State(${\it ds}_{2}$)$\rightarrow\mathbb{N}\rightarrow$Prop), $f$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$$T$).
\-\\[0ex]weak{-}precond{-}send{-}p(${\it es}$;$T$;$\mathbb{N}$;$l_{1}$;${\it tg}$;$a$;${\it ds}_{1}$;$\lambda$$s$,$m$. $\neg$$P$($s$,$m$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $P$($s$,$n$));$f$)
\\[0ex]$\Rightarrow$ weak{-}precond{-}send{-}p(${\it es}$;$\mathbb{N}$;$\mathbb{N}$;$l_{2}$;${\it tg}$;$a$;${\it ds}_{2}$;$\lambda$$s$,$m$. $\neg$$Q$($s$,$m$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $Q$($s$,$n$));$\lambda$$s$,$m$. $m$)
\\[0ex]$\Rightarrow$ destination($l_{1}$) $=$ source($l_{2}$) $\in$ Id
\\[0ex]$\Rightarrow$ destination($l_{2}$) $=$ source($l_{1}$) $\in$ Id
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{1}$), $k$:$\mathbb{N}$. Dec($P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{2}$), $k$:$\mathbb{N}$. Dec($Q$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @source($l_{1}$) stable $s$.$P$($s$,$k$)  )
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @source($l_{2}$) stable $s$.$Q$($s$,$k$)  )
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:$\mathbb{N}$.\+
\\[0ex]$\forall$$e$@source($l_{1}$).
\\[0ex]$P$(state after $e$,$k$)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@destination($l_{1}$).$Q$((state when ${\it e'}$),$k$) $\vee$ ($\forall$$n$:$\mathbb{N}$. $Q$(state after ${\it e'}$,$n$)))
\-\\[0ex]$\Rightarrow$ ($\forall$$e$:E. kind($e$) $=$ rcv($l_{2}$,${\it tg}$) $\in$ Knd $\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. $k$$<$val($e$) $\Rightarrow$ $P$(state after $e$,$k$)))
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:$\mathbb{N}$, $e$:E.\+
\\[0ex]kind($e$) $=$ rcv($l_{1}$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ val($e$) $=$ $f$((state when sender($e$)),$k$)
\\[0ex]$\Rightarrow$ $Q$(state after $e$,$k$))
\-\\[0ex]$\Rightarrow$ $\exists$$e$@destination($l_{1}$).True
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. $\exists$$e$@destination($l_{1}$).($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $Q$((state when $e$),$n$)) $\vee$ ($\forall$$n$:$\mathbb{N}$. $Q$(state after $e$,$n$)))
\end{tabbing}